deferred logic { . } : int ~> int
where forall x. { x } = 0

lemma : forall y. { y } + { y } = 0
